YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(nil()) -> nil()
  , f(.(nil(), y)) -> .(nil(), f(y))
  , f(.(.(x, y), z)) -> f(.(x, .(y, z)))
  , g(nil()) -> nil()
  , g(.(x, nil())) -> .(g(x), nil())
  , g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

Trs: { g(nil()) -> nil() }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
        [f](x1) = [1] x1 + [0]         
                                       
          [nil] = [0]                  
                                       
    [.](x1, x2) = [1] x1 + [1] x2 + [0]
                                       
        [g](x1) = [1] x1 + [1]         
  
  This order satisfies the following ordering constraints:
  
            [f(nil())] =  [0]                        
                       >= [0]                        
                       =  [nil()]                    
                                                     
      [f(.(nil(), y))] =  [1] y + [0]                
                       >= [1] y + [0]                
                       =  [.(nil(), f(y))]           
                                                     
    [f(.(.(x, y), z))] =  [1] y + [1] x + [1] z + [0]
                       >= [1] y + [1] x + [1] z + [0]
                       =  [f(.(x, .(y, z)))]         
                                                     
            [g(nil())] =  [1]                        
                       >  [0]                        
                       =  [nil()]                    
                                                     
      [g(.(x, nil()))] =  [1] x + [1]                
                       >= [1] x + [1]                
                       =  [.(g(x), nil())]           
                                                     
    [g(.(x, .(y, z)))] =  [1] y + [1] x + [1] z + [1]
                       >= [1] y + [1] x + [1] z + [1]
                       =  [g(.(.(x, y), z))]         
                                                     

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(nil()) -> nil()
  , f(.(nil(), y)) -> .(nil(), f(y))
  , f(.(.(x, y), z)) -> f(.(x, .(y, z)))
  , g(.(x, nil())) -> .(g(x), nil())
  , g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Weak Trs: { g(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

Trs: { f(nil()) -> nil() }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
        [f](x1) = [1] x1 + [2]         
                                       
          [nil] = [2]                  
                                       
    [.](x1, x2) = [1] x1 + [1] x2 + [1]
                                       
        [g](x1) = [1] x1 + [2]         
  
  This order satisfies the following ordering constraints:
  
            [f(nil())] =  [4]                        
                       >  [2]                        
                       =  [nil()]                    
                                                     
      [f(.(nil(), y))] =  [1] y + [5]                
                       >= [1] y + [5]                
                       =  [.(nil(), f(y))]           
                                                     
    [f(.(.(x, y), z))] =  [1] y + [1] x + [1] z + [4]
                       >= [1] y + [1] x + [1] z + [4]
                       =  [f(.(x, .(y, z)))]         
                                                     
            [g(nil())] =  [4]                        
                       >  [2]                        
                       =  [nil()]                    
                                                     
      [g(.(x, nil()))] =  [1] x + [5]                
                       >= [1] x + [5]                
                       =  [.(g(x), nil())]           
                                                     
    [g(.(x, .(y, z)))] =  [1] y + [1] x + [1] z + [4]
                       >= [1] y + [1] x + [1] z + [4]
                       =  [g(.(.(x, y), z))]         
                                                     

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(.(nil(), y)) -> .(nil(), f(y))
  , f(.(.(x, y), z)) -> f(.(x, .(y, z)))
  , g(.(x, nil())) -> .(g(x), nil())
  , g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Weak Trs:
  { f(nil()) -> nil()
  , g(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

Trs: { g(.(x, nil())) -> .(g(x), nil()) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
        [f](x1) = [1] x1 + [0]         
                                       
          [nil] = [1]                  
                                       
    [.](x1, x2) = [1] x1 + [1] x2 + [0]
                                       
        [g](x1) = [2] x1 + [2]         
  
  This order satisfies the following ordering constraints:
  
            [f(nil())] =  [1]                        
                       >= [1]                        
                       =  [nil()]                    
                                                     
      [f(.(nil(), y))] =  [1] y + [1]                
                       >= [1] y + [1]                
                       =  [.(nil(), f(y))]           
                                                     
    [f(.(.(x, y), z))] =  [1] y + [1] x + [1] z + [0]
                       >= [1] y + [1] x + [1] z + [0]
                       =  [f(.(x, .(y, z)))]         
                                                     
            [g(nil())] =  [4]                        
                       >  [1]                        
                       =  [nil()]                    
                                                     
      [g(.(x, nil()))] =  [2] x + [4]                
                       >  [2] x + [3]                
                       =  [.(g(x), nil())]           
                                                     
    [g(.(x, .(y, z)))] =  [2] y + [2] x + [2] z + [2]
                       >= [2] y + [2] x + [2] z + [2]
                       =  [g(.(.(x, y), z))]         
                                                     

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(.(nil(), y)) -> .(nil(), f(y))
  , f(.(.(x, y), z)) -> f(.(x, .(y, z)))
  , g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Weak Trs:
  { f(nil()) -> nil()
  , g(nil()) -> nil()
  , g(.(x, nil())) -> .(g(x), nil()) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

Trs: { f(.(nil(), y)) -> .(nil(), f(y)) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
        [f](x1) = [2] x1 + [0]         
                                       
          [nil] = [2]                  
                                       
    [.](x1, x2) = [1] x1 + [1] x2 + [0]
                                       
        [g](x1) = [2] x1 + [0]         
  
  This order satisfies the following ordering constraints:
  
            [f(nil())] =  [4]                        
                       >  [2]                        
                       =  [nil()]                    
                                                     
      [f(.(nil(), y))] =  [2] y + [4]                
                       >  [2] y + [2]                
                       =  [.(nil(), f(y))]           
                                                     
    [f(.(.(x, y), z))] =  [2] y + [2] x + [2] z + [0]
                       >= [2] y + [2] x + [2] z + [0]
                       =  [f(.(x, .(y, z)))]         
                                                     
            [g(nil())] =  [4]                        
                       >  [2]                        
                       =  [nil()]                    
                                                     
      [g(.(x, nil()))] =  [2] x + [4]                
                       >  [2] x + [2]                
                       =  [.(g(x), nil())]           
                                                     
    [g(.(x, .(y, z)))] =  [2] y + [2] x + [2] z + [0]
                       >= [2] y + [2] x + [2] z + [0]
                       =  [g(.(.(x, y), z))]         
                                                     

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(.(.(x, y), z)) -> f(.(x, .(y, z)))
  , g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Weak Trs:
  { f(nil()) -> nil()
  , f(.(nil(), y)) -> .(nil(), f(y))
  , g(nil()) -> nil()
  , g(.(x, nil())) -> .(g(x), nil()) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.

Trs: { g(.(x, .(y, z))) -> g(.(.(x, y), z)) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA) and not(IDA(1)).
  
        [f](x1) = [1 1] x1 + [0]           
                  [0 0]      [1]           
                                           
          [nil] = [0]                      
                  [0]                      
                                           
    [.](x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                  [0 1]      [0 0]      [1]
                                           
        [g](x1) = [2 0] x1 + [2]           
                  [2 1]      [0]           
  
  This order satisfies the following ordering constraints:
  
            [f(nil())] =  [0]                              
                          [1]                              
                       >= [0]                              
                          [0]                              
                       =  [nil()]                          
                                                           
      [f(.(nil(), y))] =  [1 1] y + [1]                    
                          [0 0]     [1]                    
                       >= [1 1] y + [1]                    
                          [0 0]     [1]                    
                       =  [.(nil(), f(y))]                 
                                                           
    [f(.(.(x, y), z))] =  [1 1] y + [1 1] x + [1 1] z + [2]
                          [0 0]     [0 0]     [0 0]     [1]
                       >= [1 1] y + [1 1] x + [1 1] z + [2]
                          [0 0]     [0 0]     [0 0]     [1]
                       =  [f(.(x, .(y, z)))]               
                                                           
            [g(nil())] =  [2]                              
                          [0]                              
                       >  [0]                              
                          [0]                              
                       =  [nil()]                          
                                                           
      [g(.(x, nil()))] =  [2 0] x + [2]                    
                          [2 1]     [1]                    
                       >= [2 0] x + [2]                    
                          [2 1]     [1]                    
                       =  [.(g(x), nil())]                 
                                                           
    [g(.(x, .(y, z)))] =  [2 2] y + [2 0] x + [2 2] z + [4]
                          [2 2]     [2 1]     [2 2]     [3]
                       >  [2 2] y + [2 0] x + [2 2] z + [2]
                          [2 2]     [2 1]     [2 2]     [2]
                       =  [g(.(.(x, y), z))]               
                                                           

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs: { f(.(.(x, y), z)) -> f(.(x, .(y, z))) }
Weak Trs:
  { f(nil()) -> nil()
  , f(.(nil(), y)) -> .(nil(), f(y))
  , g(nil()) -> nil()
  , g(.(x, nil())) -> .(g(x), nil())
  , g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.

Trs: { f(.(.(x, y), z)) -> f(.(x, .(y, z))) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA) and not(IDA(1)).
  
        [f](x1) = [2 0] x1 + [0]           
                  [1 0]      [3]           
                                           
          [nil] = [2]                      
                  [0]                      
                                           
    [.](x1, x2) = [1 2] x1 + [1 0] x2 + [0]
                  [0 0]      [0 1]      [1]
                                           
        [g](x1) = [1 2] x1 + [0]           
                  [0 0]      [1]           
  
  This order satisfies the following ordering constraints:
  
            [f(nil())] =  [4]                              
                          [5]                              
                       >  [2]                              
                          [0]                              
                       =  [nil()]                          
                                                           
      [f(.(nil(), y))] =  [2 0] y + [4]                    
                          [1 0]     [5]                    
                       >  [2 0] y + [2]                    
                          [1 0]     [4]                    
                       =  [.(nil(), f(y))]                 
                                                           
    [f(.(.(x, y), z))] =  [2 4] y + [2 4] x + [2 0] z + [4]
                          [1 2]     [1 2]     [1 0]     [5]
                       >  [2 4] y + [2 4] x + [2 0] z + [0]
                          [1 2]     [1 2]     [1 0]     [3]
                       =  [f(.(x, .(y, z)))]               
                                                           
            [g(nil())] =  [2]                              
                          [1]                              
                       >= [2]                              
                          [0]                              
                       =  [nil()]                          
                                                           
      [g(.(x, nil()))] =  [1 2] x + [4]                    
                          [0 0]     [1]                    
                       >= [1 2] x + [4]                    
                          [0 0]     [1]                    
                       =  [.(g(x), nil())]                 
                                                           
    [g(.(x, .(y, z)))] =  [1 2] y + [1 2] x + [1 2] z + [4]
                          [0 0]     [0 0]     [0 0]     [1]
                       >= [1 2] y + [1 2] x + [1 2] z + [4]
                          [0 0]     [0 0]     [0 0]     [1]
                       =  [g(.(.(x, y), z))]               
                                                           

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { f(nil()) -> nil()
  , f(.(nil(), y)) -> .(nil(), f(y))
  , f(.(.(x, y), z)) -> f(.(x, .(y, z)))
  , g(nil()) -> nil()
  , g(.(x, nil())) -> .(g(x), nil())
  , g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))